1. Technical Field
The present invention relates to computer program analysis and more particularly to a system and method for monotonic partial order reduction in evaluation of concurrent programs.
2. Description of the Related Art
In concurrent systems, like device drivers, the number of interleavings of transitions from different threads or processes can be very large. This results in large state spaces and makes verification difficult for concurrent programs. Existing partial order reduction methods for pruning redundant interleavings during verification are either non-optimal, not accurate enough or not suited for symbolic implementation.
Existing partial order reduction methods for pruning redundant interleaving during verification are based either on computing persistent sets by using static analysis to compute the set of dependencies. Since static analysis typically over-approximates the set of behaviors of the given program, it may over-estimate the set of dependencies between transitions—making these techniques non-optimal. Moreover, these methods are not easy to incorporate in a symbolic model checking framework.
In explicit-state model checking, partial order reduction (POR) techniques have been developed to exploit the equivalence of interleavings of independent transitions in order to reduce the search state space. Since computing the precise dependence relation may be as hard as verification itself, existing POR methods often use a conservative static analysis to compute an approximation for it. Dynamic and Cartesian partial order reduction obviate the need for applying static analysis a priori by detecting collisions (data dependencies) on-the-fly. These methods can, in general, achieve more reduction due to the more accurate collision detection. However, applying these POR methods (which were designed for explicit-state algorithms) to symbolic model checking is a non-trivial task.
A major strength of SAT-based (satisfiability-based) symbolic methods is that property dependent and data dependent search space reduction is automatically exploited inside modern SAT or SMT (Satisfiability Modulo Theory) solvers, through the addition of conflict clauses and non-chronological backtracking. Symbolic methods are often more efficient in reasoning about variables with large domains. However, combining classic POR methods (e.g., those based on persistent-sets) with symbolic algorithms has proven to be difficult. The difficulty arises from the fact that symbolic methods implicitly manipulate large sets of states as opposed to manipulating states individually. Capturing and exploiting transitions that are dynamically independent with respect to a set of states is much harder than for individual states.
Consider the example program shown in FIG. 1 comprised of two concurrent threads accessing a global array α[ ] and an interleaving lattice 20. The two pointers p and q may be aliased. Statically, transitions tA, tB in thread T1 are dependent with tar tα, tβ in T2. Therefore, POR methods relying on a static analysis may be ineffective. Note that when i≠j holds in some executions, tA,tB and tα,tβ become independent, meaning that the two sequences tA; tB; tα; tβ; tC; tγ; and tα; tβ; tA, tB; tC; tγ; are equivalent. However, none of the existing symbolic partial order reduction methods takes advantage of such information.
Among explicit-state POR methods, dynamic partial order reduction and Cartesian partial order reduction are able to achieve some reduction by detecting conflicts on-the-fly. In any individual state s, the values of i and j (as well as p and q) are fully determined, making it much easier to detect conflicts. However, it is not clear how to directly apply these techniques to symbolic model checking, where conflict detection is performed with respect to a set of states. Missing out on these kind of partial-order reductions can be costly, since a symbolic model checker needs to exhaustively search among the reduced set of execution sequences. The number of valid interleavings (sequences) can be large even for moderate sized programs.
Recently, a new technique called Peephole Partial Order Reduction (PPOR) has been proposed that allows partial order reduction to be integrated with symbolic state space exploration techniques. The key idea behind PPOR is to place constraints on which processes can be scheduled to execute in the next two steps starting at each global state. If in a global state, transitions tr and tr′ such that tid(tr)<tid(tr′), where tid denotes thread-id, are enabled and independent then tr′ cannot execute immediately before tr. It was shown that PPOR is optimal for programs with two threads but non-optimal for programs with more than two. The reason is that to achieve optimality for programs with more than two threads, we might need to track dependency chains involving many processes. These chains, which could be spread out over an entire computation, are hard to capture via local scheduling constraints.